(0) Obligation:
Clauses:
f(A, [], RES) :- g(A, [], RES).
f(.(A, As), .(B, Bs), RES) :- f(.(B, .(A, As)), Bs, RES).
g([], RES, RES).
g(.(C, Cs), D, RES) :- g(Cs, .(C, D), RES).
Query: f(g,g,a)
(1) PrologToDTProblemTransformerProof (SOUND transformation)
Built DT problem from termination graph DT10.
(2) Obligation:
Triples:
gA(.(X1, X2), X3, X4, X5) :- gA(X2, X1, .(X3, X4), X5).
gB(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, X8))))))), X9, X10) :- gA(X8, X7, .(X6, .(X5, .(X4, .(X3, .(X2, .(X1, .(X9, []))))))), X10).
fC(.(X1, X2), [], X3) :- gB(X2, X1, X3).
fC(.(X1, X2), .(X3, []), X4) :- gB(.(X1, X2), X3, X4).
fC(.(X1, X2), .(X3, .(X4, X5)), X6) :- fC(.(X4, .(X3, .(X1, X2))), X5, X6).
Clauses:
gcA([], X1, X2, .(X1, X2)).
gcA(.(X1, X2), X3, X4, X5) :- gcA(X2, X1, .(X3, X4), X5).
gcB([], X1, .(X1, [])).
gcB(.(X1, []), X2, .(X1, .(X2, []))).
gcB(.(X1, .(X2, [])), X3, .(X2, .(X1, .(X3, [])))).
gcB(.(X1, .(X2, .(X3, []))), X4, .(X3, .(X2, .(X1, .(X4, []))))).
gcB(.(X1, .(X2, .(X3, .(X4, [])))), X5, .(X4, .(X3, .(X2, .(X1, .(X5, [])))))).
gcB(.(X1, .(X2, .(X3, .(X4, .(X5, []))))), X6, .(X5, .(X4, .(X3, .(X2, .(X1, .(X6, []))))))).
gcB(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, [])))))), X7, .(X6, .(X5, .(X4, .(X3, .(X2, .(X1, .(X7, [])))))))).
gcB(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, X8))))))), X9, X10) :- gcA(X8, X7, .(X6, .(X5, .(X4, .(X3, .(X2, .(X1, .(X9, []))))))), X10).
fcC([], [], []).
fcC(.(X1, X2), [], X3) :- gcB(X2, X1, X3).
fcC(.(X1, X2), .(X3, []), X4) :- gcB(.(X1, X2), X3, X4).
fcC(.(X1, X2), .(X3, .(X4, X5)), X6) :- fcC(.(X4, .(X3, .(X1, X2))), X5, X6).
Afs:
fC(x1, x2, x3) = fC(x1, x2)
(3) TriplesToPiDPProof (SOUND transformation)
We use the technique of [DT09]. With regard to the inferred argument filtering the predicates were used in the following modes:
fC_in: (b,b,f)
gB_in: (b,b,f)
gA_in: (b,b,b,f)
Transforming
TRIPLES into the following
Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:
FC_IN_GGA(.(X1, X2), [], X3) → U3_GGA(X1, X2, X3, gB_in_gga(X2, X1, X3))
FC_IN_GGA(.(X1, X2), [], X3) → GB_IN_GGA(X2, X1, X3)
GB_IN_GGA(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, X8))))))), X9, X10) → U2_GGA(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, gA_in_ggga(X8, X7, .(X6, .(X5, .(X4, .(X3, .(X2, .(X1, .(X9, []))))))), X10))
GB_IN_GGA(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, X8))))))), X9, X10) → GA_IN_GGGA(X8, X7, .(X6, .(X5, .(X4, .(X3, .(X2, .(X1, .(X9, []))))))), X10)
GA_IN_GGGA(.(X1, X2), X3, X4, X5) → U1_GGGA(X1, X2, X3, X4, X5, gA_in_ggga(X2, X1, .(X3, X4), X5))
GA_IN_GGGA(.(X1, X2), X3, X4, X5) → GA_IN_GGGA(X2, X1, .(X3, X4), X5)
FC_IN_GGA(.(X1, X2), .(X3, []), X4) → U4_GGA(X1, X2, X3, X4, gB_in_gga(.(X1, X2), X3, X4))
FC_IN_GGA(.(X1, X2), .(X3, []), X4) → GB_IN_GGA(.(X1, X2), X3, X4)
FC_IN_GGA(.(X1, X2), .(X3, .(X4, X5)), X6) → U5_GGA(X1, X2, X3, X4, X5, X6, fC_in_gga(.(X4, .(X3, .(X1, X2))), X5, X6))
FC_IN_GGA(.(X1, X2), .(X3, .(X4, X5)), X6) → FC_IN_GGA(.(X4, .(X3, .(X1, X2))), X5, X6)
R is empty.
The argument filtering Pi contains the following mapping:
fC_in_gga(
x1,
x2,
x3) =
fC_in_gga(
x1,
x2)
.(
x1,
x2) =
.(
x1,
x2)
[] =
[]
gB_in_gga(
x1,
x2,
x3) =
gB_in_gga(
x1,
x2)
gA_in_ggga(
x1,
x2,
x3,
x4) =
gA_in_ggga(
x1,
x2,
x3)
FC_IN_GGA(
x1,
x2,
x3) =
FC_IN_GGA(
x1,
x2)
U3_GGA(
x1,
x2,
x3,
x4) =
U3_GGA(
x1,
x2,
x4)
GB_IN_GGA(
x1,
x2,
x3) =
GB_IN_GGA(
x1,
x2)
U2_GGA(
x1,
x2,
x3,
x4,
x5,
x6,
x7,
x8,
x9,
x10,
x11) =
U2_GGA(
x1,
x2,
x3,
x4,
x5,
x6,
x7,
x8,
x9,
x11)
GA_IN_GGGA(
x1,
x2,
x3,
x4) =
GA_IN_GGGA(
x1,
x2,
x3)
U1_GGGA(
x1,
x2,
x3,
x4,
x5,
x6) =
U1_GGGA(
x1,
x2,
x3,
x4,
x6)
U4_GGA(
x1,
x2,
x3,
x4,
x5) =
U4_GGA(
x1,
x2,
x3,
x5)
U5_GGA(
x1,
x2,
x3,
x4,
x5,
x6,
x7) =
U5_GGA(
x1,
x2,
x3,
x4,
x5,
x7)
We have to consider all (P,R,Pi)-chains
Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES
(4) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
FC_IN_GGA(.(X1, X2), [], X3) → U3_GGA(X1, X2, X3, gB_in_gga(X2, X1, X3))
FC_IN_GGA(.(X1, X2), [], X3) → GB_IN_GGA(X2, X1, X3)
GB_IN_GGA(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, X8))))))), X9, X10) → U2_GGA(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, gA_in_ggga(X8, X7, .(X6, .(X5, .(X4, .(X3, .(X2, .(X1, .(X9, []))))))), X10))
GB_IN_GGA(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, X8))))))), X9, X10) → GA_IN_GGGA(X8, X7, .(X6, .(X5, .(X4, .(X3, .(X2, .(X1, .(X9, []))))))), X10)
GA_IN_GGGA(.(X1, X2), X3, X4, X5) → U1_GGGA(X1, X2, X3, X4, X5, gA_in_ggga(X2, X1, .(X3, X4), X5))
GA_IN_GGGA(.(X1, X2), X3, X4, X5) → GA_IN_GGGA(X2, X1, .(X3, X4), X5)
FC_IN_GGA(.(X1, X2), .(X3, []), X4) → U4_GGA(X1, X2, X3, X4, gB_in_gga(.(X1, X2), X3, X4))
FC_IN_GGA(.(X1, X2), .(X3, []), X4) → GB_IN_GGA(.(X1, X2), X3, X4)
FC_IN_GGA(.(X1, X2), .(X3, .(X4, X5)), X6) → U5_GGA(X1, X2, X3, X4, X5, X6, fC_in_gga(.(X4, .(X3, .(X1, X2))), X5, X6))
FC_IN_GGA(.(X1, X2), .(X3, .(X4, X5)), X6) → FC_IN_GGA(.(X4, .(X3, .(X1, X2))), X5, X6)
R is empty.
The argument filtering Pi contains the following mapping:
fC_in_gga(
x1,
x2,
x3) =
fC_in_gga(
x1,
x2)
.(
x1,
x2) =
.(
x1,
x2)
[] =
[]
gB_in_gga(
x1,
x2,
x3) =
gB_in_gga(
x1,
x2)
gA_in_ggga(
x1,
x2,
x3,
x4) =
gA_in_ggga(
x1,
x2,
x3)
FC_IN_GGA(
x1,
x2,
x3) =
FC_IN_GGA(
x1,
x2)
U3_GGA(
x1,
x2,
x3,
x4) =
U3_GGA(
x1,
x2,
x4)
GB_IN_GGA(
x1,
x2,
x3) =
GB_IN_GGA(
x1,
x2)
U2_GGA(
x1,
x2,
x3,
x4,
x5,
x6,
x7,
x8,
x9,
x10,
x11) =
U2_GGA(
x1,
x2,
x3,
x4,
x5,
x6,
x7,
x8,
x9,
x11)
GA_IN_GGGA(
x1,
x2,
x3,
x4) =
GA_IN_GGGA(
x1,
x2,
x3)
U1_GGGA(
x1,
x2,
x3,
x4,
x5,
x6) =
U1_GGGA(
x1,
x2,
x3,
x4,
x6)
U4_GGA(
x1,
x2,
x3,
x4,
x5) =
U4_GGA(
x1,
x2,
x3,
x5)
U5_GGA(
x1,
x2,
x3,
x4,
x5,
x6,
x7) =
U5_GGA(
x1,
x2,
x3,
x4,
x5,
x7)
We have to consider all (P,R,Pi)-chains
(5) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LOPSTR] contains 2 SCCs with 8 less nodes.
(6) Complex Obligation (AND)
(7) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
GA_IN_GGGA(.(X1, X2), X3, X4, X5) → GA_IN_GGGA(X2, X1, .(X3, X4), X5)
R is empty.
The argument filtering Pi contains the following mapping:
.(
x1,
x2) =
.(
x1,
x2)
GA_IN_GGGA(
x1,
x2,
x3,
x4) =
GA_IN_GGGA(
x1,
x2,
x3)
We have to consider all (P,R,Pi)-chains
(8) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.
(9) Obligation:
Q DP problem:
The TRS P consists of the following rules:
GA_IN_GGGA(.(X1, X2), X3, X4) → GA_IN_GGGA(X2, X1, .(X3, X4))
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(10) QDPSizeChangeProof (EQUIVALENT transformation)
By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.
From the DPs we obtained the following set of size-change graphs:
- GA_IN_GGGA(.(X1, X2), X3, X4) → GA_IN_GGGA(X2, X1, .(X3, X4))
The graph contains the following edges 1 > 1, 1 > 2
(11) YES
(12) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
FC_IN_GGA(.(X1, X2), .(X3, .(X4, X5)), X6) → FC_IN_GGA(.(X4, .(X3, .(X1, X2))), X5, X6)
R is empty.
The argument filtering Pi contains the following mapping:
.(
x1,
x2) =
.(
x1,
x2)
FC_IN_GGA(
x1,
x2,
x3) =
FC_IN_GGA(
x1,
x2)
We have to consider all (P,R,Pi)-chains
(13) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.
(14) Obligation:
Q DP problem:
The TRS P consists of the following rules:
FC_IN_GGA(.(X1, X2), .(X3, .(X4, X5))) → FC_IN_GGA(.(X4, .(X3, .(X1, X2))), X5)
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(15) QDPSizeChangeProof (EQUIVALENT transformation)
By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.
From the DPs we obtained the following set of size-change graphs:
- FC_IN_GGA(.(X1, X2), .(X3, .(X4, X5))) → FC_IN_GGA(.(X4, .(X3, .(X1, X2))), X5)
The graph contains the following edges 2 > 2
(16) YES